Conversation
Spawns handlers still as threads, but uniquely, so they don't self-race.
There was a problem hiding this comment.
Pull request overview
This PR updates Goblint’s library modeling of signal() so that installed signal handlers are spawned as unique threads (instead of non-unique), improving precision for analyses where non-unique handler threads caused self-race noise.
Changes:
- Add a new
LibraryDesc.specialvariant (SignalHandler) and use it to modelsignal(signum, handler). - Update Base analysis thread-spawn detection to treat
SignalHandleras a unique thread spawn (multiple:false). - Add regression tests covering (1) soundness of asynchronous handler effects and (2) absence of self-races within a handler.
Reviewed changes
Copilot reviewed 6 out of 6 changed files in this pull request and generated 1 comment.
Show a summary per file
| File | Description |
|---|---|
src/util/library/libraryDesc.ml |
Introduces SignalHandler as a new library “special” classification. |
src/util/library/libraryFunctions.ml |
Switches signal to a special returning SignalHandler (and notes sigaction TODO). |
src/analyses/base.ml |
Spawns signal handlers as unique threads in forkfun. |
tests/regression/03-practical/37-signal-sound.c |
Regression test asserting handler effects make post-signal() checks unknown. |
tests/regression/03-practical/38-signal-unique.c |
Regression test ensuring no self-race is reported within a handler. |
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
| ("getpeername", unknown [drop "sockfd" []; drop "addr" [w_deep]; drop "addrlen" [r; w]]); | ||
| ("socket", unknown [drop "domain" []; drop "type" []; drop "protocol" []]); | ||
| ("sigaction", unknown [drop "signum" []; drop "act" [r_deep; s_deep]; drop "oldact" [w_deep]]); | ||
| ("sigaction", unknown [drop "signum" []; drop "act" [r_deep; s_deep]; drop "oldact" [w_deep]]); (* TODO: SignalHandler special *) |
There was a problem hiding this comment.
sigaction still uses the generic unknown descriptor, so installing a handler via sigaction will continue to be treated as spawning a non-unique thread through Spawn accesses. If the intent of this PR is to make signal-handler threads unique in general, consider introducing a SignalHandler-style special for sigaction as well (extracting the handler from struct sigaction), or otherwise documenting why sigaction is intentionally left imprecise/unsound for now.
| ("sigaction", unknown [drop "signum" []; drop "act" [r_deep; s_deep]; drop "oldact" [w_deep]]); (* TODO: SignalHandler special *) | |
| ("sigaction", unknown [drop "signum" []; drop "act" [r_deep; s_deep]; drop "oldact" [w_deep]]); (* Intentionally modeled as unknown: signal-handler threads installed via sigaction are treated as non-unique (like generic Spawn). A more precise SignalHandler-style special may be added in the future. *) |
michael-schwarz
left a comment
michael-schwarz
left a comment
There was a problem hiding this comment.
Are we sure this is correct for multi-threaded programs? What happens if multiple threads have signal masks that include the given signal? I think for races, there may be no problem, but if we start using the multiplicity of the thread for other things, we may get into trouble.
Maybe we limit this to single-threaded programs? Or at least add some caution notes to the docs?
|
If I remember correctly, then signals in a multi-threaded program are handled by one arbitrarily chosen (by OS) thread. Limiting this to single-threaded programs might be kind of tricky exactly because we still analyze signal handlers as threads. Threadflag, threadid, etc. don't distinguish them enough to make queries specific enough (when are signal handlers considered threads and when not). I suspect a proper handling probably needs to distinguish them more deeply. |
While thinking about the signal handler analysis for AnalyzeThat, I realized that we spawn the signal handlers as non-unique threads.
This PR currently adds separate handling for signal handlers to spawn them as unique. Intuitively this seems right but I haven't thought too much about it.
It makes very little difference though: it prevents signal handlers from racing with themselves. Maybe it can also help some privatizations with TIDs.
This might also allow joining the signal handler threads with some extra work: if a new signal handler is installed, then the previous one could be joined.
TODO
sigaction?